g:IGroup, a:|g|. ~(~(a)) = a 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, IMonoid, IGroup
Lemmas	igrp wf, grp car wf, grp inv wf, grp op cancel l, grp inverse, grp id wf